\section{Properties}
\label{Section:Properties}
In this Section~\ref{Section:Properties} are reported the three properties we have proved in their decidable TRIO formulation. 

In order to verify these properties with Spin we needed to translate them from their ``present/future'' formulation to a ``present/past'' formulation because of some inherent limitations of Spin. The latter property has been verified only with Zot that doesn't need any time translation.

\begin{lstlisting}[language=TRIO,basicstyle=\small,breaklines,breakatwhitespace,frame=single,caption=Property 1,label=Code:Property1]
actualGear = First & controlGearShift = TCUShiftOneUp -> Futr(actualGear = Second, FluidDelay + ShiftDelay);
\end{lstlisting}

\begin{lstlisting}[language=TRIO,basicstyle=\small,breaklines,breakatwhitespace,frame=single,caption=Property 2,label=Code:Property2]
actualGear = First & gearHandle = HandleShiftReverse -> Futr(actualGear = Reverse, FluidDelay + ShiftDelay) & Lasts_ii(transmissionShaftState = Detached, FluidDelay + ShiftDelay));
\end{lstlisting}

\begin{lstlisting}[language=TRIO,basicstyle=\small,breaklines,breakatwhitespace,frame=single,caption=Property 3,label=Code:Property3]
actualGear = First & gearHandle = HandleShiftPark -> Futr(actualGear = Park, FluidDelay + ShiftDelay) & Until(transmissionShaftState = Detached, gearHandle <> Nothing));
\end{lstlisting}

These three properties are available in their Zot formulation directly in Listings~\ref{Code:ComputerControlledAutomaticTransmission3}.

Log files resulting from our verifications are available at this page \url{http://code.google.com/p/ccat/source/browse/#svn/trunk/log}.